Nuprl Lemma : reverse_append
2,24
postcript
pdf
T
:Type,
as
,
bs
:
T
List. rev(
as
@
bs
) = (rev(
bs
) @ rev(
as
))
T
List
latex
Definitions
as
@
bs
,
True
,
T
,
rev(
as
)
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
append
back
nil
,
reverse
wf
,
squash
wf
,
true
wf
,
append
wf
,
append
assoc
origin
T:Type, as, bs:T List. rev(as @ bs) = (rev(bs) @ rev(as)) 
T List T:Type, as, bs:T List. rev(as @ bs) = (rev(bs) @ rev(as)) T List 
T
Q
Q Q Tx:A. B(x)